 Process
Analysis Toolkit (PAT) 3.5
Help |
The Unified Modeling Language (UML) has been known as the de facto standard
of software modeling language. However, the deficiency of precise and complete
semantics, especially for dynamic behavior, impedes the ability to guarantee the
correctness of UML models, which has raised many concerns on integrating formal
methods with the verification. UML state machines are used to describe the behavior and interaction of
software components. It depicts the various states that an object may be in and
the transitions between those states. We provide a translation approach
from state machines to CSP#, so as to perform simulation and
verification using PAT. This section will present a short tutorial on analyzing UML state
machines using PAT.
Copyright © 2007-2012 Semantic Engineering Pte. Ltd.